\begin{tabbing}
crossed{-}pair\{i:l\}(${\it es}$;${\it ff}$;${\it is\_req}$;${\it is\_ack}$;${\it sndr}$;${\it rcvr}$;$r$;$a$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=${\it ff}$.S(${\it sndr}$,${\it rcvr}$,$r$)\+
\\[0ex]\& ${\it is\_req}$($r$)
\\[0ex]\& ${\it ff}$.S(${\it rcvr}$,${\it sndr}$,$a$)
\\[0ex]\& ${\it is\_ack}$($a$)
\\[0ex]\& ($\exists$\=${\it r'}$:\{$e$:E$\mid$ ${\it ff}$.R(${\it rcvr}$,$e$)\} \+
\\[0ex]$\exists$\=${\it a'}$:\{$e$:E$\mid$ ${\it ff}$.R(${\it sndr}$,$e$)\} \+
\\[0ex](${\it ff}$.Sender(${\it rcvr}$,${\it r'}$) = $r$ \& ${\it ff}$.Sender(${\it sndr}$,${\it a'}$) = $a$ \& ($r$ $<$ ${\it a'}$) \& ($a$ $<$ ${\it r'}$)))
\-\-\-
\end{tabbing}